“School of Computer Science”
Back to Papers HomeBack to Papers of School of Computer Science
| Paper IPM / Computer Science / 10872 |
|
| Abstract: | |
|
It is shown that the intuitionistic theory of polynomial induction on positive ?1b (coNP) formulas does not prove the sentence ��?x, yz = y(x = - y - ? x = - z - ). This implies the unprovability of the scheme ��PIND(S1b+) in the mentioned theory. However, this theory contains the sentence ?x, y��z = y(x = - y - ? x = - z - ). The above independence result is proved by constructing an ?-chain of submodels of a countable model of S2 + O3 + �exp such that none of the worlds in the chain satisfies the sentence, and interpreting the chain as a Kripke model.
Download TeX format |
|
| back to top | |
